Conversation
PR summary 6f37e001ee
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.SpecialFunctions.Bessel | 2782 | 2797 | +15 (+0.54%) |
| Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric | 2780 | 2781 | +1 (+0.04%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric |
1 |
Mathlib.Analysis.SpecialFunctions.Bessel |
15 |
Declarations diff (regex)
+ Multiset.nnnorm_prod_map
+ Multiset.norm_prod_map
+ analyticOnNhd_tsum_besselJ_mul_pow
+ besselJ_mul_pow_le
+ deriv_regularizedHGFun
+ hasSum_besselJ_mul_pow
+ mul_deriv_besselJ_eq_besselJ_add_one
+ mul_deriv_besselJ_eq_besselJ_add_one_int
+ mul_deriv_besselJ_eq_besselJ_sub_one
+ mul_deriv_besselJ_eq_besselJ_sub_one_int
+ mul_regularizedHGFunCoeff
+ mul_regularizedHGFunCoeff_of_mem_right
+ norm_Gamma_le_norm_Gamma_add_of_one_le_re
+ norm_Gamma_le_norm_Gamma_add_one
+ norm_besselJ_le_exp
+ norm_besselJ_le_exp_int
+ regularizedHGFun_le_exp_of_one_le_re
+ regularizedHGFun_zero_singleton_eq_mul_add_mul
+ regularizedHGFun_zero_singleton_eq_mul_add_mul_aux
+ summable_besselJ_mul_pow
+ summable_bound
+ summable_deriv_HGF
+ tsum_besselJ_mul_pow
+ two_mul_deriv_besselJ
+ two_mul_deriv_besselJ_int
+ two_mul_self_mul_besselJ
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean)
✅ Lean-aware diff — post-build, computed from the Lean environment (commit
6f37e00).
- +24 new declarations
- −0 removed declarations
+Complex.analyticOnNhd_tsum_besselJ_mul_pow
+Complex.deriv_regularizedHGFun
+Complex.hasSum_besselJ_mul_pow
+Complex.mul_deriv_besselJ_eq_besselJ_add_one
+Complex.mul_deriv_besselJ_eq_besselJ_add_one_int
+Complex.mul_deriv_besselJ_eq_besselJ_sub_one
+Complex.mul_deriv_besselJ_eq_besselJ_sub_one_int
+Complex.mul_regularizedHGFunCoeff
+Complex.mul_regularizedHGFunCoeff_of_mem_right
+Complex.norm_Gamma_le_norm_Gamma_add_of_one_le_re
+Complex.norm_Gamma_le_norm_Gamma_add_one
+Complex.norm_besselJ_le_exp
+Complex.norm_besselJ_le_exp_int
+Complex.regularizedHGFun_le_exp_of_one_le_re
+Complex.regularizedHGFun_zero_singleton_eq_mul_add_mul
+Complex.summable_besselJ_mul_pow
+Complex.tsum_besselJ_mul_pow
+Complex.two_mul_deriv_besselJ
+Complex.two_mul_deriv_besselJ_int
+Complex.two_mul_self_mul_besselJ
+Multiset.nnnorm_prod_map
+Multiset.norm_prod_map
+nnnormHom.congr_simp
+normHom.congr_simpNo changes to strong technical debt.
No changes to weak technical debt.
Current commit 6f37e001ee
Reference commit fd634dd297
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
wwylele
changed the title
3723751 to
c693d60
Compare
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
Two derivative recurrences have incorrect DLMF references, alongside minor naming and spelling issues.
Get a fresh assessment by requesting another Copilot review.
Review effort: Balanced
Findings: 3
Open (3)
What changed in this PR
Adds the generating function for integer-order Bessel functions, supported by recurrence, derivative, convergence, and norm-bound lemmas.
Changes:
- Adds Bessel recurrence and derivative identities.
- Proves summability, analyticity, and the Bessel generating function.
- Adds supporting hypergeometric, Gamma, and multiset norm lemmas.
| File | Description |
|---|---|
Mathlib/Analysis/SpecialFunctions/Bessel.lean |
Proves recurrences, bounds, and generating function. |
Mathlib/Analysis/SpecialFunctions/RegularizedHypergeometric.lean |
Adds coefficient, derivative, and norm bounds. |
Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean |
Adds Gamma norm-growth bounds. |
Mathlib/Analysis/Normed/Ring/Basic.lean |
Adds multiset product norm lemmas. |
Mathlib/Analysis/Calculus/FDeriv/Analytic.lean |
Registers analytic derivatives for fun_prop. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
This proves$e^{\frac{1}{2}z(t-t^{-1})}=\sum_{m=-\infty}^{\infty}t^{m}J_{m}\left(z\right)$